Propositions as some Types